T:Type, L:(T List).
((null(L)))  no_repeats(T;L)  (x:T. last(L) before x  L  False) 

latex

ProofTree

Definitions	s = t, t  T, x:AB(x), P  Q, x:A. B(x), last(L), Type, type List, A, no_repeats(T;l), x before y  l, P  Q, x:A  B(x), P & Q, P  Q, Void, x:A.B(x), Top, S  T, null(as), b, False, (x  l), , x:A. B(x), L1  L2,
Lemmas	l before transitivity, l before member, before last, l member wf, l before wf, false wf, no repeats wf, not wf, assert wf, null wf3, member wf, top wf, no repeats iff, last wf